update-spec-decl(upd;ds) == z:Id. (z  update-spec-vars(upd))  z  dom(ds) 

latex

---

clarification:

update-spec-decl(upd;ds) == z:Id. (z  update-spec-vars(upd)  Id)  fpf-dom(IdDeq; z; ds) 

latex

Definitions	x:A. B(x), P  Q, (x  l), update-spec-vars(upd), Id, b, x  dom(f), IdDeq
FDL editor aliases	update-spec-decl